Search

At present, formal methods significantly facilitate the specification and verification of security requirements in requirement engineering, which can reduce requirement errors in the early stage of system development. Extracting formal specifications from security requirements and then evaluating the quality of the requirements are regarded as a promising solution to ensure software quality. Propositional projection temporal logic (PPTL) with a strong mathematical basis and full regular expressiveness is a suitable language for formal specifications. Inspired by natural language processing and text mining techniques, this paper designs and implements a tool, namely, NL2PPTL, to generate formal coarse‐grained and fine‐grained specifications in terms of PPTL formulas automatically. In specific, the grammatical production rules are defined to construct the syntax tree, and then, the formula is obtained by post‐order traversal of the tree. The satisfiability of the PPTL specifications can be checked utilizing PPTLSAT. In addition, the state transformation model is constructed from fine‐grained specifications, so as to discover scope conflicts and verify the security properties of the requirement case. [ABSTRACT FROM AUTHOR]

Real-time audio/video transmission through Internet media is an important part of communication. Due to bandwidth limitations and a noisy environment, delivery of multimedia content to a remote location is not 100% guaranteed. These limitations are the basic cause of missing packets which affect the Quality of Service (QoS). A protocol for the recovery of lost packets is described in [Maxemchuk, Nicholas F., K. Padmanabhan, and S. Lo. “A cooperative packet recovery protocol for multicast video.” Network Protocols, 1997. Proc. of 1997 International Conference on. IEEE]. This protocol claims significant improvement in QoS. We formally specify the protocol in a network of timed automata. By model-checking (A mathematical technique), we find that packet recovery is not always there. In this article, We report such scenarios of malfunctioning in the protocol when the size of multimedia contents is known (e.g., live video/audio broadcasting) and middle-level servers have different rates of data sending and receiving. We formulate the effect of inter-packet delay and transmission speed difference on a buffer.

Attestation is one of the most critical mechanisms in confidential computing (CC). We present a holistic verification approach enabling comprehensive and rigorous security analysis of architecturally-defined attestation mechanisms in CC. Specifically, we analyze two prominent next-generation hardware-based Trusted Execution Environments (TEEs), namely Arm Confidential Compute Architecture (CCA) and Intel Trust Domain Extensions (TDX). For both of these solutions, we provide a comprehensive specification of all phases of the attestation mechanism, namely provisioning, initialization, and attestation protocol. We demonstrate that including the initialization phase in the formal model leads to a violation of integrity, freshness, and secrecy properties for Intel’s claimed trusted computing base (TCB), which could not be captured by considering the attestation protocol alone in the related work. We open-source our artifacts. Other researchers, including a team from Intel, are adopting our artifacts for further analysis.

The Unified Modeling Language (UML) is a standard for modeling dynamic systems. UML behavioral state machines are used for modeling the dynamic behavior of object-oriented designs. The UML specification, maintained by the Object Management Group (OMG), is documented in natural language (in contrast to formal language). The inherent ambiguity of natural languages may introduce inconsistencies in the resulting statemachine model. Formalizing UML state machine specification aims at solving the ambiguity problem and at providing a uniform view to software designers and developers. Such a formalization also aims at providing a foundation for automatic verification of UML state machine models, which can help to find software design vulnerabilities at an early stage and reduce the development cost. We provide here a comprehensive survey of existing work from 1997 to 2021 related to formalizing UML state machine semantics for the purpose of conducting model checking at the design stage. [ABSTRACT FROM AUTHOR]

In recent years, the field of security requirements specification by formal methods has changed radically. The security requirement specification is now one of the widely recognized as well as actively pursued research challenges in both requirement engineering and security engineering communities. In this paper, we focus on the research metadata to find the state of the art in the field of security requirements specification using the formal approach. In order, a review was taken up to perform metadata, obtained from frequently used databases. In total, 200 publications were retrieved; out of which 110 were found to be relevant to our research questions. The results of metadata provided an insight into the main contributions of the field, research gaps, and challenges, which motivated the discussion for important research direction in the future. [ABSTRACT FROM AUTHOR]

Team formation in an environment where some relevant parameters are not known in advance is a challenging problem. Communicating automata and distributed algorithms have been used to describe protocols for team formation. A high‐level specification provides a mathematical description of a protocol or a program. TLA +$$ {}^{+} $$ is a formal specification language designed to provide high‐level specifications of concurrent and distributed systems. The associated model checker known as TLC is capable of model checking the TLA +$$ {}^{+} $$ specifications. Recently, formal specification of a team formation protocol is given using TLA +$$ {}^{+} $$ when there is a single initiator (an agent or a robot) that initiates the team formation. Using TLA +$$ {}^{+} $$, we examine the formal specification for the multiple initiator situation and demonstrate that a composition technique can yield a single monolithic specification for the multiple initiator situation from the single initiator situation specification. We have used models of varying sizes, and the TLC model checker has confirmed that the protocol's specifications meet certain desired characteristics in each case. [ABSTRACT FROM AUTHOR]

Abstract Formal methods are proven techniques that provide a rigorous mathematical basis to software development. In particular, they allow the quality of development to be effectively improved by making accurate and explicit modelling, so that anomalies like ambiguities and incompleteness are identified in the early phases of the software development process. Semi‐formal UML models and formal Timed Automata models are used to design a telerehabilitation system through a practical approach based on abstraction and refinement. The formal verification of expected properties of the system is performed by the Uppaal tool. The motivation of this work is threefold: (i) showing the usefulness of formal methods to satisfy the validation needs of a medical telerehabilitation system; (ii) demonstrating our approach of system analysis through refinements to guide the development of a complex system; and (iii) highlighting, from a real‐life experience, the usefulness of models to involve the stakeholders all along the design of a system, from requirements to detailed specifications.

The European Railway Agency has formulated assumptions for a target model of rail transport. Its important premise is digitalization to support the communication and transport services that the railways will make available to the public in the future. Part of the digitalization process is the digital description of the railway infrastructure in a formalized form to allow algorithmic processing. The formal description of infrastructure is not a new issue. However, attempts made so far have not resulted in a permanent definition of a generally accessible formalism allowing for a coherent representation of the physical railway infrastructure in a digital form. This paper presents the results of work carried out within the research project Digital Railway-The Digital Twin of the ETCS Application-Virtual Prototyping and Simulation of Operational Scenarios.

In this paper, we aim to contribute to the knowledge about how imperative C functions can be transformed to Maude functional and system modules respectively. Maude is a formal specification language characterized by simplicity, expressivity and good performance. It is a multi-paradigm meta-language based on rewriting logic and equational theories used to specify, simulate and formally verify concurrent and distributed systems. Maude has been used to define the operational semantics of many programming and specification languages. In particular, the addition of this paper is to close the gap between a subset of the C standard language and Maude relying on a transformational approach.

Abstract Software faults are costly to find and remove from programs. It is better to avoid inserting the faults in the first place. The authors identify requirements‐related faults that can arise during the transformation of formal specifications into programs, analyse each to discover its causes, and propose corresponding fault prevention methods. The approach works by analysing a specification, decomposing it into specification fragments with different levels like components, determining the correct implementation order among the components, and enabling automated code generation for the components and other low‐level specification fragments. The approach seeks to reduce the faults in programs significantly by guiding programmers to work effectively and productively. The authors evaluate the approach's performance experimentally and compare it to the performance of a fault‐prevention method with industry applications.

Formal methods are proven techniques that provide a rigorous mathematical basis to software development. In particular, they allow the quality of development to be effectively improved by making accurate and explicit modelling, so that anomalies like ambiguities and incompleteness are identified in the early phases of the software development process. Semi‐formal UML models and formal Timed Automata models are used to design a telerehabilitation system through a practical approach based on abstraction and refinement. The formal verification of expected properties of the system is performed by the Uppaal tool. The motivation of this work is threefold: (i) showing the usefulness of formal methods to satisfy the validation needs of a medical telerehabilitation system; (ii) demonstrating our approach of system analysis through refinements to guide the development of a complex system; and (iii) highlighting, from a real‐life experience, the usefulness of models to involve the stakeholders all along the design of a system, from requirements to detailed specifications. [ABSTRACT FROM AUTHOR]

Software faults are costly to find and remove from programs. It is better to avoid inserting the faults in the first place. The authors identify requirements‐related faults that can arise during the transformation of formal specifications into programs, analyse each to discover its causes, and propose corresponding fault prevention methods. The approach works by analysing a specification, decomposing it into specification fragments with different levels like components, determining the correct implementation order among the components, and enabling automated code generation for the components and other low‐level specification fragments. The approach seeks to reduce the faults in programs significantly by guiding programmers to work effectively and productively. The authors evaluate the approach's performance experimentally and compare it to the performance of a fault‐prevention method with industry applications. [ABSTRACT FROM AUTHOR]

Abstract The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grained automatic modelling for Java source programs. By the principle that the execution details of property‐unchecked, non‐interactive, and unrelated statements do not affect the model checking results, we model coarse‐grained model fragments for such statements, while fine‐grained model fragments for property‐checked, interactive, and related statements. Our method reduces the model and state space and ensures the error detection of the source program based on model checking. Moreover, we prove the equivalence of the fine‐grained model, the coarse‐grained model, and the program. Finally, this paper gives an experiment to verify the effectiveness of the proposed method.

In an article published in IEEE Access in 2020, researchers present an approach to using TLA+ for the formal verification of whether a network of SDN (Software-Defined Networking) switches implements the filtering rules of a given monolithic firewall. The distributed as well as monolithic firewalls are specified with TLA+. It is shown that the correctness of the former with respect to the latter can be verified automatically by using the TLC model checker. The main contributions of this paper are the following improvements of that approach. Firstly, by specifying switches without using any variables, the time needed for the model checking is reduced significantly. For example, the verification of the same networks takes a few seconds with the new approach and does not end after several hours with the previous one. Secondly, the following problem is solved. With the latter, if a monolithic firewall allows a packet to pass through, all the paths in the distributed firewall which the packet is routed on must allow the same. Otherwise, the model checker proclaims the distributed firewall to be in error. We present an additional approach to the verification, which gives a positive answer if at least one of the paths allows the packet to pass through.

Summary: The automation of programming, which lies at the intersection of software engineering and artificial intelligence, enables machines to automatically generate programs that satisfy given requirements. In the context of B formal design modeling, one of the challenges is the refactoring of substitutions in design specifications, which often uses state transitions to describe how program or system statuses change during execution. This paper proposes a condition and substitution refactoring algorithm for the B formal specification language. The aim of the work is to automatically derive B operational predicates based on given transitions. The work has been extremely useful to machine‐driven formal design model repair as well as automated design specification generation. Given a set of state transitions, common relations of their state variables can be discovered and clustered into a number of classes. These relations can be further used to synthesize substitutions that derive new states from existing states. To restrict application domains of the synthesized substitutions, conditions that guard these substitutions are generated using first‐order logic. We have implemented the proposed algorithm as an extension to the ProB model checker. Experiments were conducted based on the B model public dataset. The evaluation results demonstrated that our solution is able to synthesize conditions and substitutions for various sets of state transitions in a wide range of B models. [ABSTRACT FROM AUTHOR]

The European Railway Agency has formulated assumptions for a target model of rail transport. Its important premise is digitalization to support the communication and transport services that the railways will make available to the public in the future. Part of the digitalization process is the digital description of the railway infrastructure in a formalized form to allow algorithmic processing. The formal description of infrastructure is not a new issue. However, attempts made so far have not resulted in a permanent definition of a generally accessible formalism allowing for a coherent representation of the physical railway infrastructure in a digital form. This paper presents the results of work carried out within the research project Digital Railway-The Digital Twin of the ETCS Application-Virtual Prototyping and Simulation of Operational Scenarios. [ABSTRACT FROM AUTHOR]

Autonomous driving systems are crucial complicated cyber–physical systems that combine physical environment awareness with cognitive computing. Deep reinforcement learning is currently commonly used in the decision-making of such systems. However, black-box-based deep reinforcement learning systems do not guarantee system safety and the interpretability of the reward-function settings in the face of complex environments and the influence of uncontrolled uncertainties. Therefore, a formal security reinforcement learning method is proposed. First, we propose an environmental modeling approach based on the influence of nondeterministic environmental factors, which enables the precise quantification of environmental issues. Second, we use the environment model to formalize the reward machine's structure, which is used to guide the reward-function setting in reinforcement learning. Third, we generate a control barrier function to ensure a safer state behavior policy for reinforcement learning. Finally, we verify the method's effectiveness in intelligent driving using overtaking and lane-changing scenarios. [ABSTRACT FROM AUTHOR]

The state space explosion restricts the error detection of concurrent software. The abstraction can provide a solution to avoid state space explosion, but it is easy to ignore important details, resulting in inaccurate detection results. This paper proposes a methodology of fine‐coarse‐grained automatic modelling for Java source programs. By the principle that the execution details of property‐unchecked, non‐interactive, and unrelated statements do not affect the model checking results, we model coarse‐grained model fragments for such statements, while fine‐grained model fragments for property‐checked, interactive, and related statements. Our method reduces the model and state space and ensures the error detection of the source program based on model checking. Moreover, we prove the equivalence of the fine‐grained model, the coarse‐grained model, and the program. Finally, this paper gives an experiment to verify the effectiveness of the proposed method. [ABSTRACT FROM AUTHOR]

This paper proposes an approach to the specification and model checking of a large, important class of distributed algorithms called control algorithms (CAs), which are superimposed on underlying distributed systems (UDSs). The approach is based on rewriting logic by moving from its object level to the meta-level. We introduce the idea of specifying CAs as meta-programs that take the specifications of UDSs and automatically generate the specifications of the UDSs on which the CAs are superimposed (UDS-CAs). Due to many options, such as network topologies, even fixing the number of each kind of entities, such as mobile support stations (MSSs) and mobile hosts (MHs) in a mobile checkpointing algorithm, there are many instances of a UDS. To address the problem, we generate all possible initial states of a UDS for a fixed number of each kind of entities such that some constraints, such as MSSs strongly connected with a wired network, are fulfilled and conduct model checking for each of the initial states. We demonstrate the usefulness by reporting on a case study where a counterexample is found for some specific initial states but not for the other initial states, detecting a subtle flaw lurking in a mobile checkpointing algorithm. [ABSTRACT FROM AUTHOR]

Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. In this work, we consider the description of the expected behaviour of a Ladder program under the form of a timing chart, describing a scenario of execution. Our aim is to prove that the given Ladder program conforms to the expected temporal behaviour given by such a timing chart. Our approach amounts to translating the Ladder code, together with the timing chart, into a program for the Why3 environment for deductive program verification. The verification proceeds with the generation of verification conditions: mathematical formulas to be checked valid using automated theorem provers. The ultimate goal is twofold. On the one hand, by obtaining a complete proof, one verifies the conformity of the Ladder code with respect to the timing chart with a high degree of confidence. On the other hand, in the case the proof is not fully completed, one obtains a counterexample, illustrating a possible execution scenario of the Ladder code which does not conform to the timing chart. [ABSTRACT FROM AUTHOR]

Abstract Non‐functional requirements define qualities of the software system that ensure effectiveness while embedding any constraints and restrictions on the design. A challenge rises with agile implementation in handling non‐function requirements in regulated environments. Thus, a practitioner's perceptions of agile method tailoring are described in relation to inter‐team boundaries and non‐functional requirements. The research comprises 18 practitioner interviews from two multinational agile software development companies. Interviews were recorded, transcribed, and analysed using an approach informed by grounded theory and information flow models were used to compare and contrast interactions of processes. It was discovered that one of the case study companies managed non‐functional requirements as artefacts in their agile methodology, while the other company reverts to conventional plan‐based software development practices of documentation, timeline estimations, and safety critical requirements. This research creates a detailed comparison of these contrasting approaches. The main contribution of this study is a set of proposed recommendations to deal with non‐functional requirements in a regulated environment using agile techniques. The introduction of two new artefacts, Documentation Work Item and Safety Critical Work Item, is recommended and it is accompanied with an illustrative example, to transform the handling of documentation and safety critical requirements in a more agile way.

Abstract The dependability characteristic of the control software of manufacturing systems is highlighted more than before, going through repeated changes to cope with various and varying requirements. Formal methods are researched to be applied to automation system engineering to obtain a more effective and efficient quality assurance. One of the approaches, a formal specification language named Generalised Test Tables has been developed with the aim of intuitiveness and accessibility for automation application developers. The result of the experiments conducted to assess the usability of this language is presented here. Focussing on evaluating effectiveness and user satisfaction, three paper‐based experiments have been conducted with students at the bachelor and master level. The evaluation results point to positive usability in both comparative effectiveness to conventional language, that is, Petri Nets, and subjective perception of user satisfaction.